ds:(IdType), da:(IdKndType), Aa, Ba, Ab, Bb:Type, Ca:Component(ds;da;Aa;Ba),
Cb:Component(ds;da;Ab;Bb), Pa:ComponentSpec(Aa;Ba), Pb:ComponentSpec(Ab;Bb).
component-compatible(ds;da;Aa;Ab;Ca;Cb)
 component-output-disjoint{i:l}(ds;da;Aa;Ab;Ca;Cb)
 Ca |- es,in,out.Pa(es,in,out)
 Cb |- es,in,out.Pb(es,in,out)
 mux-component(Ca;Cb) |- es,in,out.Pa(es,es-interface-left(in),es-interface-left(out))
 mux-component(Ca;Cb) |- es,in,out.& Pb(es,es-interface-right(in),es-interface-right(out)) 

latex

Definitions

A c B, P & Q, es-decl(es;ds;da), t  ...$L, x,y,z. t(x;y;z), x. t(x), t.1, t.2, Top, t  T, , mux-component(Ca;Cb), x(s1,s2,s3), C |- es,in,out.P(es;in;out), P  Q, ComponentSpec(A;B), x:A. B(x), x(s), component-output-disjoint{i:l}(ds;da;T1;T2;C1;C2), component-compatible(ds;da;T1;T2;C1;C2), Component(ds;da;A;B)

Lemmas

union-interface-right, abs-interface-right, union-interface-left, abs-interface-left, es-interface-right wf, interface-union wf, es-interface-left wf, scheme-plus wf, scheme-implies-rule, es-kindtype wf, hasloc wf, assert wf, es-state wf, scheme-and-rule, Knd wf, Id wf, component wf, component-compatible wf, top wf, component-subtype, component-output-disjoint wf, es-interface wf, component-realizes wf, scheme-compatible wf, es-interface-disjoint wf, event system wf, abs-interface wf, scheme-realizes wf, interface wf, RealizerScheme wf, es-decl wf, interface-right wf, subtype rel sum, interface-subtype, interface-left wf